BackThruLemma `assert\_of\_tt`